Nuprl Definition : l_subset
11,40
postcript
pdf
l_subset(
T
;
as
;
bs
) ==
x
:
T
. (
x
as
)
(
x
bs
)
latex
clarification:
l_subset(
T
;
as
;
bs
) ==
x
:
T
. (
x
as
T
)
(
x
bs
T
)
latex
Definitions
x
:
A
.
B
(
x
)
,
P
Q
,
(
x
l
)
FDL editor aliases
l_subset
origin
x:T. (x 
as) 
(x bs)
x:T. (x as T) (x bs T) x:T. (x as) (x bs)
x:T. (x as T) (x bs T) x:A. B(x) Q l)